\begin{tabbing}
$M$.sends($k$,$s$,$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$concat(map\=($\lambda$${\it pL}$.tagged{-}messages((${\it pL}$.1).2;$s$;$v$;${\it pL}$.2)\+
\\[0ex];fpf{-}vals(product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);$\lambda$$p$.\=eqof(KindDeq)\+
\\[0ex](($p$.1)
\\[0ex],$k$);($M$.2.2.2.2.2).1)))
\-\-
\end{tabbing}